Nuprl Lemma : refl_cl_sp_cancel
13,42
postcript
pdf
T
:Type,
r
:(
T
T
).
dec_binrel(
T
;
x
,
y
:
T
.
x
=
y
T
)
refl(
T
;
r
)
anti_sym(
T
;
r
)
(((
r
\)
) <
>{
T
}
r
)
latex
Up
gen
algebra
1
Definitions
x
,
y
.
t
(
x
;
y
)
,
t
T
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
x
(
s1
,
s2
)
Lemmas
ab
binrel
wf
,
dec
binrel
wf
,
xxrefl
wf
,
xxanti
sym
wf
,
s
part
wf
,
refl
cl
wf
,
binrel
le
antisymmetry
,
refl
cl
sp
le
rel
,
rel
le
refl
cl
sp
origin
T:Type, r:(T
T
).
T) 
refl(T;r) anti_sym(T;r) (((r\)
) <
>{T} r) T:Type, r:(TT).
T) refl(T;r) anti_sym(T;r) (((r\)) <>{T} r) 
x,y. t(x;y) T Qx:A. B(x)